es:ES, Cmd:Type, In:AbsInterface(Cmd), isupdate:(Cmd), Sys, Out:AbsInterface(Top).
(E(In) r E(Sys))
 (f:sys-antecedent(es;Sys).
 (e:E(In). f(e) = e  E)
  (chain:(E(Sys)(Id List)).
  chain-consistent(f;chain)  (x, y:E(Sys). x is f*(y)  loc(x) <<= loc(y)))) 

latex

Up	abstract chain replication
Definitions	, t  T, P  Q, x <<= y, x:A. B(x), E(X)
Lemmas	chain-order wf, es-loc wf